package tr.edu.ege.kipler.satisfiability.syntactical;

import tr.edu.ege.kipler.syntax.concept.BinaryConcept;
import tr.edu.ege.kipler.syntax.concept.Concept;
import tr.edu.ege.kipler.syntax.concept.ConceptName;
import tr.edu.ege.kipler.syntax.concept.ConceptVisitor;
import tr.edu.ege.kipler.syntax.concept.ModalConcept;
import tr.edu.ege.kipler.syntax.concept.Nominal;
import tr.edu.ege.kipler.syntax.concept.QualifiedNoRestriction;
import tr.edu.ege.kipler.syntax.concept.RoleQuantification;
import tr.edu.ege.kipler.syntax.concept.BinaryConcept.Constructor;

/**
 * 
 * @author İnanç Seylan
 *
 */
public class ConceptSimplificationVisitor implements ConceptVisitor {
	private Concept normalForm;

	public Concept getNormalForm() {
		return normalForm;
	}

	public void visitBinaryConcept(BinaryConcept bd) {
		normalForm = bd;
		ConceptSimplificationVisitor visitor = new ConceptSimplificationVisitor();
		bd.getLhs().accept(visitor);
		bd.setLhs(visitor.getNormalForm());
		visitor = new ConceptSimplificationVisitor();
		bd.getRhs().accept(visitor);
		bd.setRhs(visitor.getNormalForm());
		if (bd.getConstructor() == Constructor.UNION) {
			if (bd.getLhs().equals(ConceptName.topConcept())
					|| bd.getRhs().equals(ConceptName.topConcept())) {
				normalForm = ConceptName.topConcept();
			} else if (bd.getLhs().equals(ConceptName.bottomConcept())) {
				normalForm = bd.getRhs();
			} else if (bd.getRhs().equals(ConceptName.bottomConcept())) {
				normalForm = bd.getLhs();
			}
		} else { // intersection
			if (bd.getLhs().equals(ConceptName.bottomConcept())
					|| bd.getRhs().equals(ConceptName.bottomConcept())) {
				normalForm = ConceptName.bottomConcept();
			} else if (bd.getLhs().equals(ConceptName.topConcept())) {
				normalForm = bd.getRhs();
			} else if (bd.getRhs().equals(ConceptName.topConcept())) {
				normalForm = bd.getLhs();
			}
		}
	}

	public void visitConceptName(ConceptName c) {
		// nothing to do
		normalForm = c;
	}

	public void visitRoleQuantification(RoleQuantification restriction) {
		normalForm = restriction;
		ConceptSimplificationVisitor visitor = new ConceptSimplificationVisitor();
		restriction.getConcept().accept(visitor);
		restriction.setConcept(visitor.getNormalForm());
	}

	public void visitModalConcept(ModalConcept md) {
		normalForm = md;
		ConceptSimplificationVisitor visitor = new ConceptSimplificationVisitor();
		md.getConcept().accept(visitor);
		md.setConcept(visitor.getNormalForm());
	}

	public void visitQualifiedNoRestriction(QualifiedNoRestriction restriction) {
		if (restriction.getNo() < 0) {
			normalForm = ConceptName.bottomConcept();
		} else if (restriction.getNo() == 0
				&& restriction.getConstructor() == QualifiedNoRestriction.Constructor.AT_LEAST) {
			// >=(0, R, C) <-> T
			normalForm = ConceptName.topConcept();
		} else if (restriction.getNo() == 0
				&& restriction.getConstructor() == QualifiedNoRestriction.Constructor.AT_MOST) {
			// <=(0, R, C) <-> all(R, ~C)
			ConceptSimplificationVisitor visitor = new ConceptSimplificationVisitor();
			restriction.getConcept().copy().toggleNegated().accept(visitor);
			normalForm = new RoleQuantification(
					RoleQuantification.Constructor.ALL, restriction.getRole(),
					visitor.getNormalForm());
		} else if (restriction.getNo() == 1
				&& restriction.getConstructor() == QualifiedNoRestriction.Constructor.AT_LEAST) {
			// >=(1, R, C) <-> some(R, C)
			ConceptSimplificationVisitor visitor = new ConceptSimplificationVisitor();
			restriction.getConcept().accept(visitor);
			normalForm = new RoleQuantification(
					RoleQuantification.Constructor.SOME, restriction.getRole(),
					visitor.getNormalForm());
		} else {
			ConceptSimplificationVisitor visitor = new ConceptSimplificationVisitor();
			restriction.getConcept().accept(visitor);
			restriction.setConcept(visitor.getNormalForm());
			normalForm = restriction;
		}
	}

	public void visitNominal(Nominal nominal) {
		// nothing to do
		normalForm = nominal;
	}

}
